ABS: es  es' mod es,e.P(es;e)

STM: es-p-equiv wf

STM: es-p-equiv weakening

STM: es-p-equiv inversion

STM: es-p-equiv transitivity

ABS: sub-es-pred(es;dom;e)

STM: sub-es-pred wf

ABS: sub-es-sender(es;dom;e)

STM: sub-es-sender wf

ABS: a.f(a) is c preserving on e.P(e)

STM: causale-order-preserving wf

ABS: a.f(a) is c< preserving on e.P(e)

STM: causal-order-preserving wf

COM: explanation of antecedent functions

ABS: Q f P

STM: antecedent-function wf

STM: antecedent-function functionality wrt iff

ABS: Q  f P

STM: antecedent-surjection wf

STM: antecedent-surjection functionality wrt iff

ABS: (e.P(e) a.f(a) e'.Q(e')) with R

STM: causal-bijection wf

STM: causal-bijection functionality wrt iff

STM: causal-bijection-interleaving

ABS: (e.P(e)  e'.Q(e')) with R

STM: causally-related wf

ABS: e.P(e) op e'.Q(e') with R

STM: causally-op-related wf

ABS: causal-predecessor(es;p)

STM: causal-predecessor wf

STM: causal-pred-wellfounded

STM: causal-pred-from-relation

ABS: es-r-pred{i:l}(es;d;R)

STM: es-r-pred wf

STM: es-r-pred-property

ABS: es-p-immediate-pred(es;P)

STM: es-p-immediate-pred wf

STM: decidable es-p-immediate-pred

STM: es-p-immediate-pred-wellfounded

ABS: es-r-immediate-pred(es;R;e';e)

STM: es-r-immediate-pred wf

STM: decidable es-r-immediate-pred

STM: not-r-immediate-pred

STM: es-r-immediate-pred-exists

ABS: causal-weak-predecessor(es;p)

STM: causal-weak-predecessor wf

ABS: e p< e'

STM: es-p-locl wf

ABS: e p e'

STM: es-p-le wf

STM: es-p-locl transitivity

STM: es-p-le transitivity

STM: es-p-le weakening

STM: es-p-le weakening eq

STM: es-p-locl transitivity1

STM: es-p-locl transitivity2

STM: es-p-locl-test

STM: es-causl weakening p-locl

STM: es-causle weakening p-le

STM: es-causl-p-locl-test

ABS: same-thread(es;p;e;e')

STM: same-thread wf

STM: same-thread-do-apply

STM: same-thread weakening

STM: same-thread inversion

STM: same-thread transitivity

STM: decidable same-thread

STM: thread-p-ordered

STM: thread-ordered

ABS: es-height(es;e)

STM: es-height wf

STM: es-height-causl

STM: single-threaded-relation

STM: single-threaded-relation3

ABS: single-thread-generator{i:l}(es;P;R)

STM: single-thread-generator wf

STM: cond rel equivalent

STM: cond equiv to causl

STM: generated-thread-properties

STM: generated-thread-binrel-properties

STM: generated-thread-binrel-properties2

STM: generated-thread-properties2

STM: generated-thread-properties3

STM: generated-thread-no-joins

ABS: for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes)

STM: fifo wf

ABS: FIFO

STM: FIFO wf

ABS: links2Fifo-impl(es;l1;l2;A;tg)

STM: links2Fifo-impl wf

ABS: ff.C

STM: fifoC wf

ABS: ff.T

STM: fifoT wf

ABS: ff.S

STM: fifoS wf

ABS: ff.R

STM: fifoR wf

ABS: ff.Codes

STM: fifoCodes wf

ABS: ff.Decodes

STM: fifoDecodes wf

ABS: ff.Sender

STM: fifoSender wf

STM: fifoSender-antecedent

STM: fifoSender-causes

STM: fifoSender-preserves-order

STM: fifoSender-one-one

STM: fifoSender-reverse-order

STM: fifoSender-encoding

STM: fifo-FIFO

ABS: [e: i p j]

ABS: [e: i p j]

STM: rcv-it wf

STM: rcv-it-loc

STM: snd-it wf

STM: snd-it-loc

STM: decidable snd-it

STM: decidable rcv-it

STM: snd-it-of-rcv-it

STM: fifoReceiver-exists

ABS: ff.Receiver

STM: fifoReceiver wf

STM: fifoReceiver-properties

STM: fifoReceiver-caused

STM: rcv-it-of-snd-it

STM: compose-fifo-send

ABS: fifo+

STM: fifo+ wf

ABS: fifo+property(es;codes;decodes;C;S;R;T;Req;Ack;i;f)

STM: fifo+property wf

STM: fifo+rewrite

ABS: F2F+-decls

STM: F2F+-decls wf

ABS: is_req  

STM: f2f+Req wf

ABS: is_ack 

STM: f2f+Ack wf

ABS: awaiting 

STM: f2f+Wait wf

ABS: owes_ack 

STM: f2f+Owes wf

ABS: req_dcdr

ABS: ack_dcdr

ABS: R_dcdr

ABS: S_dcdr

STM: f2f+SDcdr wf

STM: f2f+RDcdr wf

STM: f2f+AckDcdr wf

STM: f2f+ReqDcdr wf

STM: f2f+-property

STM: loc-of-req-sender

STM: loc-of-ack-sender

STM: loc-of-req-receiver

STM: loc-of-ack-receiver

ABS: plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)

STM: plus-ify wf

STM: owes ack-2-ff

STM: awaiting-2-ff

STM: owes ack-2-tt

STM: awaiting-2-tt

STM: acks-between-reqs

STM: reqs-between-acks

STM: bool-tt-or-ff

STM: the-first-event

ABS: first-event{i:l}(es;e)

STM: first-event wf

STM: first-event-property

STM: init-p-implies2

STM: req-received-before-ack

STM: req-sent-before-ack

STM: max-of-intset

STM: max-of-eventset

ABS: f2f+-pred(e',e)

STM: f2f+-pred wf

STM: f2f+-pred-field

STM: f2f+-pred-dom

STM: f2f+-pred-rng

STM: f2f+-pred-sub-causl

STM: decidable f2f+-pred

STM: f2f+-pred-alternates

STM: req-pred-ack

STM: ack-pred-req

STM: f2f+-pred-closed

STM: req-pred-ack2

STM: f2f+-pred-no-forks

STM: ack-has-f2f+-pred

STM: f2f+-pred-unique-min

STM: f2f+-pred-at-most-one-min

STM: f2f+-pred-generates-thread

ABS: f2f+-p+

STM: f2f+-p+ wf

STM: f2f+-p+-sub-causl

STM: f2f+-pred-is-immediate

STM: f2f+-p+-field

STM: f2f+-p+-equiv-causl

STM: f2f+-p+-total

STM: f2f+-req-exists

STM: f2f+-pred-preserves-order

STM: plus-ify-makes-FIFO+

ABS: f2f+-event(e)

STM: f2f+-event wf

ABS: crossed-pair{i:l}(es;ff;is_req;is_ack;sndr;rcvr;r;a)

STM: crossed-pair wf

STM: combine-causal-bijections

STM: combine-causally-related

ABS: fifo+switch

STM: fifo+switch wf

STM: combine-antecedent-surjections

STM: causal-order-preserving-interleaving

ABS: [S? codes1 : codes2]

STM: union-codes wf

STM: union-codes-property

ABS: [R ? decodes1 : decodes2]

STM: union-decodes wf

STM: union-decodes-property

STM: union-decodes-exists

STM: combine-fifo+

ABS: abs-R 

STM: abs-R wf

ABS: abs-S 

STM: abs-S wf

ABS: abs-fifo{i:l}(C;T)

STM: abs-fifo wf